T:Type, a:(T List), x:T. l_disjoint(T;[x];a)  ((x  a)) 

latex

Definitions	t  T, x:A. B(x), (x  l), A, P  Q, P  Q, P & Q, P  Q, type List, [], [car / cdr], l_disjoint(T;l1;l2), x:AB(x), x:A  B(x), Type
Lemmas	l disjoint singleton, iff functionality wrt iff, l disjoint-symmetry, l disjoint wf, not wf, l member wf